|
|
Problematika testování a verifikace softwaru pro leteckou techniku
Mačišák, Lukáš ; Chudý, Peter (oponent) ; Drahanský, Martin (vedoucí práce)
Tato diplomová práce popisuje problematiku certifikace a vývoje softwaru pro leteckou techniku se zaměřením na oblast testování a verifikace v rámci životního cyklu projektu. Práce obsahuje navrhnutý vlastní postup verifikace softwaru ve shodě s požadavky normy RTCA/DO-178B pro konkrétní aplikaci. Součásti je i ukázková realizace takových částí navrhnutého postupu, které se týkají testování softwaru. V závěru jsou popsané možnosti uplatnění navrženého postupu a zhodnocení jeho výsledků.
|
|
|
Přesné heuristiky pro vkládání šumu v nástroji SearchBestie
Kozák, David ; Smrčka, Aleš (oponent) ; Křena, Bohuslav (vedoucí práce)
Tato práce se zabývá efektivními způsoby testování vícevláknových programů psaných v jazyce Java. Pro zvýšení šance na odhalení časově závislých chyb se využívá techniky vkládání šumu, kdy dochází ke vložení dalších instrukcí do testované aplikace za účelem prozkoumání netypických proložení událostí. Pro nalezení vhodných konfigurací pro vkládání šumu byl navržen nástroj SearchBestie, který využíval nástroj ConTest pro spouštění testů a instrumentaci bytecodu. Jelikož vývoj ConTestu byl zastaven, bylo třeba najít vhodnou alternativu. V průběhu této bakalářské práce bylo dokončeno propojení SearchBestie s nástrojem RoadRunner, který ConTest nahradil. Dále došlo k navržení a implementaci nových heuristik, které umožňují šum vkládat na přesně zvolená místa v kódu. Experimenty prokázaly, že ve většině případů skutečně přesné heuristiky dosahují lepších výsledků než heuristiky využívající náhodnosti.
|
|
|
Instrumentace Java programů, kontrakty pro paralelismus
Žárský, Jan ; Křena, Bohuslav (oponent) ; Smrčka, Aleš (vedoucí práce)
Kontrakty pro paralelismus slouží k vyjádření potřebné atomicity sekvencí metod ve vícevláknových programech. Tato práce se zaměřuje na implementaci dynamického analyzátoru, který verifikuje programy napsané v jazyce Java vůči kontraktům. Podporovány jsou parametrické kontrakty se spojlery. Analyzátor je implementován jako rozšíření frameworku RoadRunner. V rámci implementace analyzátoru byla do frameworku RoadRunner přidána podpora pro získávání argumentů metod a jejich návratových hodnot. Analyzátor byl plně implementován a jeho funkčnost byla ověřena na sadě testovacích programů.
|
|
|
Efficient Representation of Program States
Jančík, Pavel ; Kofroň, Jan (vedoucí práce) ; Gargantini, Angelo (oponent) ; Barnat, Jiří (oponent)
Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
|
|
|
Instrumentace Java programů, kontrakty pro paralelismus
Žárský, Jan ; Křena, Bohuslav (oponent) ; Smrčka, Aleš (vedoucí práce)
Kontrakty pro paralelismus slouží k vyjádření potřebné atomicity sekvencí metod ve vícevláknových programech. Tato práce se zaměřuje na implementaci dynamického analyzátoru, který verifikuje programy napsané v jazyce Java vůči kontraktům. Podporovány jsou parametrické kontrakty se spojlery. Analyzátor je implementován jako rozšíření frameworku RoadRunner. V rámci implementace analyzátoru byla do frameworku RoadRunner přidána podpora pro získávání argumentů metod a jejich návratových hodnot. Analyzátor byl plně implementován a jeho funkčnost byla ověřena na sadě testovacích programů.
|
|
|
Přesné heuristiky pro vkládání šumu v nástroji SearchBestie
Kozák, David ; Smrčka, Aleš (oponent) ; Křena, Bohuslav (vedoucí práce)
Tato práce se zabývá efektivními způsoby testování vícevláknových programů psaných v jazyce Java. Pro zvýšení šance na odhalení časově závislých chyb se využívá techniky vkládání šumu, kdy dochází ke vložení dalších instrukcí do testované aplikace za účelem prozkoumání netypických proložení událostí. Pro nalezení vhodných konfigurací pro vkládání šumu byl navržen nástroj SearchBestie, který využíval nástroj ConTest pro spouštění testů a instrumentaci bytecodu. Jelikož vývoj ConTestu byl zastaven, bylo třeba najít vhodnou alternativu. V průběhu této bakalářské práce bylo dokončeno propojení SearchBestie s nástrojem RoadRunner, který ConTest nahradil. Dále došlo k navržení a implementaci nových heuristik, které umožňují šum vkládat na přesně zvolená místa v kódu. Experimenty prokázaly, že ve většině případů skutečně přesné heuristiky dosahují lepších výsledků než heuristiky využívající náhodnosti.
|
|
|
Efficient Representation of Program States
Jančík, Pavel ; Kofroň, Jan (vedoucí práce) ; Gargantini, Angelo (oponent) ; Barnat, Jiří (oponent)
Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
|
|
|
Problematika testování a verifikace softwaru pro leteckou techniku
Mačišák, Lukáš ; Chudý, Peter (oponent) ; Drahanský, Martin (vedoucí práce)
Tato diplomová práce popisuje problematiku certifikace a vývoje softwaru pro leteckou techniku se zaměřením na oblast testování a verifikace v rámci životního cyklu projektu. Práce obsahuje navrhnutý vlastní postup verifikace softwaru ve shodě s požadavky normy RTCA/DO-178B pro konkrétní aplikaci. Součásti je i ukázková realizace takových částí navrhnutého postupu, které se týkají testování softwaru. V závěru jsou popsané možnosti uplatnění navrženého postupu a zhodnocení jeho výsledků.
|
host ::
RSS.